T:Type, L:(T List). ((null(L)))  (hd(L)  L) 

latex

ProofTree

Definitions	hd(l), i <z j, i z j, l[i], Type, s ~ t, type List, A, (x  l), x:A  B(x), A  B, a < b, t  T, s = t, , Void, x:AB(x), P  Q, False, #$n, x:A. B(x), ||as||, n+m, i  j , P & Q, i  j < k, {x:A| B(x)} , {i..j}, , , A List, [car / cdr], [], left + right, P  Q, P  Q, P  Q, last(L), True, b, null(as)
Lemmas	l member wf, not wf, assert wf, null wf, select member, nat wf, int seg wf, member wf, non neg length, length wf1, le wf